Nuprl Lemma : es-le_transitivity
11,40
postcript
pdf
es
:ES,
a
,
b
,
c
:E.
a
loc
b
b
loc
c
a
loc
c
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
ES
,
E
,
e
loc
e'
Lemmas
es-le
wf
,
es-E
wf
,
event
system
wf
,
es-le-trans
origin
es:ES, a, b, c:E. a 
loc b 
b loc c a loc c es:ES, a, b, c:E. a loc b b loc c a loc c 
T Qx:A. B(x)loc e'